COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	I understand that you are interviewing potential Hertz Fellows on
C00007 ENDMK
C⊗;
I understand that you are interviewing potential Hertz Fellows on
Friday.  Here is the essence of my recommendation for Joe Weening.
The form and this have been mailed today.
.require "memo.pub[let,jmc]" source
re: Joseph Weening

	Joe Weening is strongly motivated to be immediately helpful,
sometimes at the cost of his long term interests.

	While he has been my research and teaching assistant he
has done the following:

1. He has taken charge of the manual for Jussi Ketonen's interactive
theorem prover EKL.  He has written several versions of the manual,
keeping up with all the changes.  This manual is an absolutely first
class job of clear exposition.  I have never had a student who writes
as well as Joe.

2. He has done the parser for EKL.  This is an excellent job, but
so far as I know, it doesn't contain new ideas.  Unlike the parsers
of my previous experience, it doesn't seem to have any bugs even
though the syntax allowed is quite rich.  It doesn't give mysterious
syntax errors.

3. He has made several small improvements to the operating system, and
he is one of the people who fixes it when it breaks.  This is not part
of his job.  When Joe sees something that needs to be done, he has
a tendency to go ahead and do it.

4. He has also been one of the leaders of the graduate students of
the Stanford Computer Science Department - again part of his tendency
to take charge of what he sees needs to be done.

	Joe has undertaken to do a thesis involving a practical system
for proving correctness of LISP programs.  If he succeeds, he will
unprecedentedly combine theoretical understanding of program semantics
with the ability to build practical systems.  From my point of view,
he has been somewhat slow in getting started in his theoretical work.
However, hardly any theorists really want to build useful systems,
and Joe certainly does.  Therefore, I consider that he is the best
bet yet to do genuinely useful work in program verification.

	Compared to the Hertz fellows I know, Mike Farmwald, Tom
McWilliams and Kurt Widdoes, Joe Weening is of equal ability but
more theoretically oriented.  He also shares their interest in
useful products.

	Compared to the better students in the Computer Science
Department, Joe is not as strong in theory as the best theorists.
He hasn't yet written any theoretical papers - perhaps partly
because I haven't demanded it.  He is up there with the best
practical system builders, and he is strong enough on theory so
that there is a good chance that is project will be both a theoretical
and a practical success.  This is very rare indeed.

	For these reasons I recommend him strongly.